Nuprl Lemma : Q-R-glued-empty 11,40

es:ES, QR:(EE), B:Type, f:Top. Q-R-glued(esBf; p-first([]); Q; p-first([]); R
latex


DefinitionsFalse, {x:AB(x)} , left + right, P  Q, Dec(P), Void, let x,y = A in B(x;y), t.1, E, t  T, b, AbsInterface(A), f(a), P  Q, x:AB(x), X(e), s = t, , x:AB(x), x:A  B(x), P & Q, x:AB(x), Type, e c e', <ab>, Unit, can-apply(f;x), e  X, Q ==f== P, E(X), Inj(A;B;f), f is Q-R-pre-preserving on P, {I}, Q f== P, g glues Ia:Qa f Ib:Rb, Q-R-glued(esIb_valtypefIaQaIbRb), p-first(L), ES, Top, [], , x.A(x)
Lemmastop wf, event system wf, es-E wf, it wf, es-causle wf, false wf, es-interface-val wf, decidable false

origin